Inference at * 
Iof proof for Lemma p-fun-exp-add-sq:


  A:Type, f:(A(A + Top)), x:A, m, n:.
  (can-apply(f^m;x))  ((f^n+m(x)) ~ (f^n(do-apply(f^m;x)))) 

latex

 by (InductionOnNat) 
CollapseTHEN ((UnivCD) 
CollapseTHENA (Auto)) 

latex

C1: 

C1: 1. A : Type
C1: 2. f : A(A + Top)
C1: 3. x : A
C1: 4. n : 
C1: 5. can-apply(f^0;x)
C1:   (f^n+0(x)) ~ (f^n(do-apply(f^0;x)))
C2: 

C2: 1. A : Type
C2: 2. f : A(A + Top)
C2: 3. x : A
C2: 4. m : 
C2: 5. 0 < m
C2: 6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
C2: 7. n : 
C2: 8. can-apply(f^m;x)
C2:   (f^n+m(x)) ~ (f^n(do-apply(f^m;x)))
C.

Definitions	n - m, n+m, -n, i  j , Type, s ~ t, , b, can-apply(f;x), f^n, suptype(S; T), , {x:A| B(x)} , A, False, P  Q, a < b, #$n, A  B, left + right, S  T, x:A. B(x), x:AB(x), Top, x:A.B(x), t  T, Void
Lemmas	ge wf, nat properties, nat wf, assert wf, can-apply wf, p-fun-exp wf, le wf, top wf